Nuprl Lemma : Rinit-discrete_wf
11,40
postcript
pdf
A
:es_realizer{i:l}. (
Rinit?(
A
))
(Rinit-discrete(
A
)
)
latex
Definitions
Rinit-discrete(
A
)
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
prop{i:l}
Lemmas
es
realizer
wf
,
Rinit?
wf
,
assert
wf
,
bfalse
wf
,
btrue
wf
,
Rinit-v
wf
origin